$\forall$$i$,$x$:Id, $T$:Type, $L$:(Knd List).
\\[0ex]normal{-}type\{i:l\}($T$) $\Rightarrow$ es{-}real\{i:l\}(${\it es}$.frame{-}p(${\it es}$; $i$; $T$; $x$; $L$))